0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇒, 89 ms)
↳2 Prolog
↳3 PrologToPiTRSProof (⇒, 0 ms)
↳4 PiTRS
↳5 DependencyPairsProof (⇔, 98 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 PiDP
↳9 UsableRulesProof (⇔, 0 ms)
↳10 PiDP
↳11 PiDPToQDPProof (⇒, 0 ms)
↳12 QDP
↳13 QDPSizeChangeProof (⇔, 10 ms)
↳14 YES
disC_in_g(or(and(T14, T15), T5)) → U4_g(T14, T15, T5, disC_in_g(T14))
disC_in_g(or(0, T5)) → U7_g(T5, disC_in_g(T5))
disC_in_g(or(1, T5)) → U8_g(T5, disC_in_g(T5))
disC_in_g(or(T64, T65)) → U9_g(T64, T65, conA_in_g(or(T64, T65)))
conA_in_g(and(T32, T33)) → U1_g(T32, T33, pB_in_gg(T32, T33))
pB_in_gg(T32, T33) → U2_gg(T32, T33, disC_in_g(T32))
disC_in_g(and(T76, T77)) → U10_g(T76, T77, pB_in_gg(T76, T77))
U10_g(T76, T77, pB_out_gg(T76, T77)) → disC_out_g(and(T76, T77))
disC_in_g(0) → disC_out_g(0)
disC_in_g(1) → disC_out_g(1)
U2_gg(T32, T33, disC_out_g(T32)) → pB_out_gg(T32, T33)
U2_gg(T32, T33, disC_out_g(T32)) → U3_gg(T32, T33, conA_in_g(T33))
conA_in_g(0) → conA_out_g(0)
conA_in_g(1) → conA_out_g(1)
U3_gg(T32, T33, conA_out_g(T33)) → pB_out_gg(T32, T33)
U1_g(T32, T33, pB_out_gg(T32, T33)) → conA_out_g(and(T32, T33))
U9_g(T64, T65, conA_out_g(or(T64, T65))) → disC_out_g(or(T64, T65))
U8_g(T5, disC_out_g(T5)) → disC_out_g(or(1, T5))
U7_g(T5, disC_out_g(T5)) → disC_out_g(or(0, T5))
U4_g(T14, T15, T5, disC_out_g(T14)) → disC_out_g(or(and(T14, T15), T5))
U4_g(T14, T15, T5, disC_out_g(T14)) → U5_g(T14, T15, T5, conA_in_g(T15))
U5_g(T14, T15, T5, conA_out_g(T15)) → disC_out_g(or(and(T14, T15), T5))
U5_g(T14, T15, T5, conA_out_g(T15)) → U6_g(T14, T15, T5, disC_in_g(T5))
U6_g(T14, T15, T5, disC_out_g(T5)) → disC_out_g(or(and(T14, T15), T5))
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
disC_in_g(or(and(T14, T15), T5)) → U4_g(T14, T15, T5, disC_in_g(T14))
disC_in_g(or(0, T5)) → U7_g(T5, disC_in_g(T5))
disC_in_g(or(1, T5)) → U8_g(T5, disC_in_g(T5))
disC_in_g(or(T64, T65)) → U9_g(T64, T65, conA_in_g(or(T64, T65)))
conA_in_g(and(T32, T33)) → U1_g(T32, T33, pB_in_gg(T32, T33))
pB_in_gg(T32, T33) → U2_gg(T32, T33, disC_in_g(T32))
disC_in_g(and(T76, T77)) → U10_g(T76, T77, pB_in_gg(T76, T77))
U10_g(T76, T77, pB_out_gg(T76, T77)) → disC_out_g(and(T76, T77))
disC_in_g(0) → disC_out_g(0)
disC_in_g(1) → disC_out_g(1)
U2_gg(T32, T33, disC_out_g(T32)) → pB_out_gg(T32, T33)
U2_gg(T32, T33, disC_out_g(T32)) → U3_gg(T32, T33, conA_in_g(T33))
conA_in_g(0) → conA_out_g(0)
conA_in_g(1) → conA_out_g(1)
U3_gg(T32, T33, conA_out_g(T33)) → pB_out_gg(T32, T33)
U1_g(T32, T33, pB_out_gg(T32, T33)) → conA_out_g(and(T32, T33))
U9_g(T64, T65, conA_out_g(or(T64, T65))) → disC_out_g(or(T64, T65))
U8_g(T5, disC_out_g(T5)) → disC_out_g(or(1, T5))
U7_g(T5, disC_out_g(T5)) → disC_out_g(or(0, T5))
U4_g(T14, T15, T5, disC_out_g(T14)) → disC_out_g(or(and(T14, T15), T5))
U4_g(T14, T15, T5, disC_out_g(T14)) → U5_g(T14, T15, T5, conA_in_g(T15))
U5_g(T14, T15, T5, conA_out_g(T15)) → disC_out_g(or(and(T14, T15), T5))
U5_g(T14, T15, T5, conA_out_g(T15)) → U6_g(T14, T15, T5, disC_in_g(T5))
U6_g(T14, T15, T5, disC_out_g(T5)) → disC_out_g(or(and(T14, T15), T5))
DISC_IN_G(or(and(T14, T15), T5)) → U4_G(T14, T15, T5, disC_in_g(T14))
DISC_IN_G(or(and(T14, T15), T5)) → DISC_IN_G(T14)
DISC_IN_G(or(0, T5)) → U7_G(T5, disC_in_g(T5))
DISC_IN_G(or(0, T5)) → DISC_IN_G(T5)
DISC_IN_G(or(1, T5)) → U8_G(T5, disC_in_g(T5))
DISC_IN_G(or(1, T5)) → DISC_IN_G(T5)
DISC_IN_G(or(T64, T65)) → U9_G(T64, T65, conA_in_g(or(T64, T65)))
DISC_IN_G(or(T64, T65)) → CONA_IN_G(or(T64, T65))
CONA_IN_G(and(T32, T33)) → U1_G(T32, T33, pB_in_gg(T32, T33))
CONA_IN_G(and(T32, T33)) → PB_IN_GG(T32, T33)
PB_IN_GG(T32, T33) → U2_GG(T32, T33, disC_in_g(T32))
PB_IN_GG(T32, T33) → DISC_IN_G(T32)
DISC_IN_G(and(T76, T77)) → U10_G(T76, T77, pB_in_gg(T76, T77))
DISC_IN_G(and(T76, T77)) → PB_IN_GG(T76, T77)
U2_GG(T32, T33, disC_out_g(T32)) → U3_GG(T32, T33, conA_in_g(T33))
U2_GG(T32, T33, disC_out_g(T32)) → CONA_IN_G(T33)
U4_G(T14, T15, T5, disC_out_g(T14)) → U5_G(T14, T15, T5, conA_in_g(T15))
U4_G(T14, T15, T5, disC_out_g(T14)) → CONA_IN_G(T15)
U5_G(T14, T15, T5, conA_out_g(T15)) → U6_G(T14, T15, T5, disC_in_g(T5))
U5_G(T14, T15, T5, conA_out_g(T15)) → DISC_IN_G(T5)
disC_in_g(or(and(T14, T15), T5)) → U4_g(T14, T15, T5, disC_in_g(T14))
disC_in_g(or(0, T5)) → U7_g(T5, disC_in_g(T5))
disC_in_g(or(1, T5)) → U8_g(T5, disC_in_g(T5))
disC_in_g(or(T64, T65)) → U9_g(T64, T65, conA_in_g(or(T64, T65)))
conA_in_g(and(T32, T33)) → U1_g(T32, T33, pB_in_gg(T32, T33))
pB_in_gg(T32, T33) → U2_gg(T32, T33, disC_in_g(T32))
disC_in_g(and(T76, T77)) → U10_g(T76, T77, pB_in_gg(T76, T77))
U10_g(T76, T77, pB_out_gg(T76, T77)) → disC_out_g(and(T76, T77))
disC_in_g(0) → disC_out_g(0)
disC_in_g(1) → disC_out_g(1)
U2_gg(T32, T33, disC_out_g(T32)) → pB_out_gg(T32, T33)
U2_gg(T32, T33, disC_out_g(T32)) → U3_gg(T32, T33, conA_in_g(T33))
conA_in_g(0) → conA_out_g(0)
conA_in_g(1) → conA_out_g(1)
U3_gg(T32, T33, conA_out_g(T33)) → pB_out_gg(T32, T33)
U1_g(T32, T33, pB_out_gg(T32, T33)) → conA_out_g(and(T32, T33))
U9_g(T64, T65, conA_out_g(or(T64, T65))) → disC_out_g(or(T64, T65))
U8_g(T5, disC_out_g(T5)) → disC_out_g(or(1, T5))
U7_g(T5, disC_out_g(T5)) → disC_out_g(or(0, T5))
U4_g(T14, T15, T5, disC_out_g(T14)) → disC_out_g(or(and(T14, T15), T5))
U4_g(T14, T15, T5, disC_out_g(T14)) → U5_g(T14, T15, T5, conA_in_g(T15))
U5_g(T14, T15, T5, conA_out_g(T15)) → disC_out_g(or(and(T14, T15), T5))
U5_g(T14, T15, T5, conA_out_g(T15)) → U6_g(T14, T15, T5, disC_in_g(T5))
U6_g(T14, T15, T5, disC_out_g(T5)) → disC_out_g(or(and(T14, T15), T5))
DISC_IN_G(or(and(T14, T15), T5)) → U4_G(T14, T15, T5, disC_in_g(T14))
DISC_IN_G(or(and(T14, T15), T5)) → DISC_IN_G(T14)
DISC_IN_G(or(0, T5)) → U7_G(T5, disC_in_g(T5))
DISC_IN_G(or(0, T5)) → DISC_IN_G(T5)
DISC_IN_G(or(1, T5)) → U8_G(T5, disC_in_g(T5))
DISC_IN_G(or(1, T5)) → DISC_IN_G(T5)
DISC_IN_G(or(T64, T65)) → U9_G(T64, T65, conA_in_g(or(T64, T65)))
DISC_IN_G(or(T64, T65)) → CONA_IN_G(or(T64, T65))
CONA_IN_G(and(T32, T33)) → U1_G(T32, T33, pB_in_gg(T32, T33))
CONA_IN_G(and(T32, T33)) → PB_IN_GG(T32, T33)
PB_IN_GG(T32, T33) → U2_GG(T32, T33, disC_in_g(T32))
PB_IN_GG(T32, T33) → DISC_IN_G(T32)
DISC_IN_G(and(T76, T77)) → U10_G(T76, T77, pB_in_gg(T76, T77))
DISC_IN_G(and(T76, T77)) → PB_IN_GG(T76, T77)
U2_GG(T32, T33, disC_out_g(T32)) → U3_GG(T32, T33, conA_in_g(T33))
U2_GG(T32, T33, disC_out_g(T32)) → CONA_IN_G(T33)
U4_G(T14, T15, T5, disC_out_g(T14)) → U5_G(T14, T15, T5, conA_in_g(T15))
U4_G(T14, T15, T5, disC_out_g(T14)) → CONA_IN_G(T15)
U5_G(T14, T15, T5, conA_out_g(T15)) → U6_G(T14, T15, T5, disC_in_g(T5))
U5_G(T14, T15, T5, conA_out_g(T15)) → DISC_IN_G(T5)
disC_in_g(or(and(T14, T15), T5)) → U4_g(T14, T15, T5, disC_in_g(T14))
disC_in_g(or(0, T5)) → U7_g(T5, disC_in_g(T5))
disC_in_g(or(1, T5)) → U8_g(T5, disC_in_g(T5))
disC_in_g(or(T64, T65)) → U9_g(T64, T65, conA_in_g(or(T64, T65)))
conA_in_g(and(T32, T33)) → U1_g(T32, T33, pB_in_gg(T32, T33))
pB_in_gg(T32, T33) → U2_gg(T32, T33, disC_in_g(T32))
disC_in_g(and(T76, T77)) → U10_g(T76, T77, pB_in_gg(T76, T77))
U10_g(T76, T77, pB_out_gg(T76, T77)) → disC_out_g(and(T76, T77))
disC_in_g(0) → disC_out_g(0)
disC_in_g(1) → disC_out_g(1)
U2_gg(T32, T33, disC_out_g(T32)) → pB_out_gg(T32, T33)
U2_gg(T32, T33, disC_out_g(T32)) → U3_gg(T32, T33, conA_in_g(T33))
conA_in_g(0) → conA_out_g(0)
conA_in_g(1) → conA_out_g(1)
U3_gg(T32, T33, conA_out_g(T33)) → pB_out_gg(T32, T33)
U1_g(T32, T33, pB_out_gg(T32, T33)) → conA_out_g(and(T32, T33))
U9_g(T64, T65, conA_out_g(or(T64, T65))) → disC_out_g(or(T64, T65))
U8_g(T5, disC_out_g(T5)) → disC_out_g(or(1, T5))
U7_g(T5, disC_out_g(T5)) → disC_out_g(or(0, T5))
U4_g(T14, T15, T5, disC_out_g(T14)) → disC_out_g(or(and(T14, T15), T5))
U4_g(T14, T15, T5, disC_out_g(T14)) → U5_g(T14, T15, T5, conA_in_g(T15))
U5_g(T14, T15, T5, conA_out_g(T15)) → disC_out_g(or(and(T14, T15), T5))
U5_g(T14, T15, T5, conA_out_g(T15)) → U6_g(T14, T15, T5, disC_in_g(T5))
U6_g(T14, T15, T5, disC_out_g(T5)) → disC_out_g(or(and(T14, T15), T5))
U4_G(T14, T15, T5, disC_out_g(T14)) → U5_G(T14, T15, T5, conA_in_g(T15))
U5_G(T14, T15, T5, conA_out_g(T15)) → DISC_IN_G(T5)
DISC_IN_G(or(and(T14, T15), T5)) → U4_G(T14, T15, T5, disC_in_g(T14))
U4_G(T14, T15, T5, disC_out_g(T14)) → CONA_IN_G(T15)
CONA_IN_G(and(T32, T33)) → PB_IN_GG(T32, T33)
PB_IN_GG(T32, T33) → U2_GG(T32, T33, disC_in_g(T32))
U2_GG(T32, T33, disC_out_g(T32)) → CONA_IN_G(T33)
PB_IN_GG(T32, T33) → DISC_IN_G(T32)
DISC_IN_G(or(and(T14, T15), T5)) → DISC_IN_G(T14)
DISC_IN_G(or(0, T5)) → DISC_IN_G(T5)
DISC_IN_G(or(1, T5)) → DISC_IN_G(T5)
DISC_IN_G(and(T76, T77)) → PB_IN_GG(T76, T77)
disC_in_g(or(and(T14, T15), T5)) → U4_g(T14, T15, T5, disC_in_g(T14))
disC_in_g(or(0, T5)) → U7_g(T5, disC_in_g(T5))
disC_in_g(or(1, T5)) → U8_g(T5, disC_in_g(T5))
disC_in_g(or(T64, T65)) → U9_g(T64, T65, conA_in_g(or(T64, T65)))
conA_in_g(and(T32, T33)) → U1_g(T32, T33, pB_in_gg(T32, T33))
pB_in_gg(T32, T33) → U2_gg(T32, T33, disC_in_g(T32))
disC_in_g(and(T76, T77)) → U10_g(T76, T77, pB_in_gg(T76, T77))
U10_g(T76, T77, pB_out_gg(T76, T77)) → disC_out_g(and(T76, T77))
disC_in_g(0) → disC_out_g(0)
disC_in_g(1) → disC_out_g(1)
U2_gg(T32, T33, disC_out_g(T32)) → pB_out_gg(T32, T33)
U2_gg(T32, T33, disC_out_g(T32)) → U3_gg(T32, T33, conA_in_g(T33))
conA_in_g(0) → conA_out_g(0)
conA_in_g(1) → conA_out_g(1)
U3_gg(T32, T33, conA_out_g(T33)) → pB_out_gg(T32, T33)
U1_g(T32, T33, pB_out_gg(T32, T33)) → conA_out_g(and(T32, T33))
U9_g(T64, T65, conA_out_g(or(T64, T65))) → disC_out_g(or(T64, T65))
U8_g(T5, disC_out_g(T5)) → disC_out_g(or(1, T5))
U7_g(T5, disC_out_g(T5)) → disC_out_g(or(0, T5))
U4_g(T14, T15, T5, disC_out_g(T14)) → disC_out_g(or(and(T14, T15), T5))
U4_g(T14, T15, T5, disC_out_g(T14)) → U5_g(T14, T15, T5, conA_in_g(T15))
U5_g(T14, T15, T5, conA_out_g(T15)) → disC_out_g(or(and(T14, T15), T5))
U5_g(T14, T15, T5, conA_out_g(T15)) → U6_g(T14, T15, T5, disC_in_g(T5))
U6_g(T14, T15, T5, disC_out_g(T5)) → disC_out_g(or(and(T14, T15), T5))
U4_G(T14, T15, T5, disC_out_g(T14)) → U5_G(T14, T15, T5, conA_in_g(T15))
U5_G(T14, T15, T5, conA_out_g(T15)) → DISC_IN_G(T5)
DISC_IN_G(or(and(T14, T15), T5)) → U4_G(T14, T15, T5, disC_in_g(T14))
U4_G(T14, T15, T5, disC_out_g(T14)) → CONA_IN_G(T15)
CONA_IN_G(and(T32, T33)) → PB_IN_GG(T32, T33)
PB_IN_GG(T32, T33) → U2_GG(T32, T33, disC_in_g(T32))
U2_GG(T32, T33, disC_out_g(T32)) → CONA_IN_G(T33)
PB_IN_GG(T32, T33) → DISC_IN_G(T32)
DISC_IN_G(or(and(T14, T15), T5)) → DISC_IN_G(T14)
DISC_IN_G(or(0, T5)) → DISC_IN_G(T5)
DISC_IN_G(or(1, T5)) → DISC_IN_G(T5)
DISC_IN_G(and(T76, T77)) → PB_IN_GG(T76, T77)
conA_in_g(and(T32, T33)) → U1_g(T32, T33, pB_in_gg(T32, T33))
conA_in_g(0) → conA_out_g(0)
conA_in_g(1) → conA_out_g(1)
disC_in_g(or(and(T14, T15), T5)) → U4_g(T14, T15, T5, disC_in_g(T14))
disC_in_g(or(0, T5)) → U7_g(T5, disC_in_g(T5))
disC_in_g(or(1, T5)) → U8_g(T5, disC_in_g(T5))
disC_in_g(or(T64, T65)) → U9_g(T64, T65, conA_in_g(or(T64, T65)))
disC_in_g(and(T76, T77)) → U10_g(T76, T77, pB_in_gg(T76, T77))
disC_in_g(0) → disC_out_g(0)
disC_in_g(1) → disC_out_g(1)
U1_g(T32, T33, pB_out_gg(T32, T33)) → conA_out_g(and(T32, T33))
U4_g(T14, T15, T5, disC_out_g(T14)) → disC_out_g(or(and(T14, T15), T5))
U4_g(T14, T15, T5, disC_out_g(T14)) → U5_g(T14, T15, T5, conA_in_g(T15))
U7_g(T5, disC_out_g(T5)) → disC_out_g(or(0, T5))
U8_g(T5, disC_out_g(T5)) → disC_out_g(or(1, T5))
U10_g(T76, T77, pB_out_gg(T76, T77)) → disC_out_g(and(T76, T77))
pB_in_gg(T32, T33) → U2_gg(T32, T33, disC_in_g(T32))
U5_g(T14, T15, T5, conA_out_g(T15)) → disC_out_g(or(and(T14, T15), T5))
U5_g(T14, T15, T5, conA_out_g(T15)) → U6_g(T14, T15, T5, disC_in_g(T5))
U2_gg(T32, T33, disC_out_g(T32)) → pB_out_gg(T32, T33)
U2_gg(T32, T33, disC_out_g(T32)) → U3_gg(T32, T33, conA_in_g(T33))
U6_g(T14, T15, T5, disC_out_g(T5)) → disC_out_g(or(and(T14, T15), T5))
U3_gg(T32, T33, conA_out_g(T33)) → pB_out_gg(T32, T33)
U4_G(T15, T5, disC_out_g) → U5_G(T5, conA_in_g(T15))
U5_G(T5, conA_out_g) → DISC_IN_G(T5)
DISC_IN_G(or(and(T14, T15), T5)) → U4_G(T15, T5, disC_in_g(T14))
U4_G(T15, T5, disC_out_g) → CONA_IN_G(T15)
CONA_IN_G(and(T32, T33)) → PB_IN_GG(T32, T33)
PB_IN_GG(T32, T33) → U2_GG(T33, disC_in_g(T32))
U2_GG(T33, disC_out_g) → CONA_IN_G(T33)
PB_IN_GG(T32, T33) → DISC_IN_G(T32)
DISC_IN_G(or(and(T14, T15), T5)) → DISC_IN_G(T14)
DISC_IN_G(or(0, T5)) → DISC_IN_G(T5)
DISC_IN_G(or(1, T5)) → DISC_IN_G(T5)
DISC_IN_G(and(T76, T77)) → PB_IN_GG(T76, T77)
conA_in_g(and(T32, T33)) → U1_g(pB_in_gg(T32, T33))
conA_in_g(0) → conA_out_g
conA_in_g(1) → conA_out_g
disC_in_g(or(and(T14, T15), T5)) → U4_g(T15, T5, disC_in_g(T14))
disC_in_g(or(0, T5)) → U7_g(disC_in_g(T5))
disC_in_g(or(1, T5)) → U8_g(disC_in_g(T5))
disC_in_g(or(T64, T65)) → U9_g(conA_in_g(or(T64, T65)))
disC_in_g(and(T76, T77)) → U10_g(pB_in_gg(T76, T77))
disC_in_g(0) → disC_out_g
disC_in_g(1) → disC_out_g
U1_g(pB_out_gg) → conA_out_g
U4_g(T15, T5, disC_out_g) → disC_out_g
U4_g(T15, T5, disC_out_g) → U5_g(T5, conA_in_g(T15))
U7_g(disC_out_g) → disC_out_g
U8_g(disC_out_g) → disC_out_g
U10_g(pB_out_gg) → disC_out_g
pB_in_gg(T32, T33) → U2_gg(T33, disC_in_g(T32))
U5_g(T5, conA_out_g) → disC_out_g
U5_g(T5, conA_out_g) → U6_g(disC_in_g(T5))
U2_gg(T33, disC_out_g) → pB_out_gg
U2_gg(T33, disC_out_g) → U3_gg(conA_in_g(T33))
U6_g(disC_out_g) → disC_out_g
U3_gg(conA_out_g) → pB_out_gg
conA_in_g(x0)
disC_in_g(x0)
U1_g(x0)
U4_g(x0, x1, x2)
U7_g(x0)
U8_g(x0)
U10_g(x0)
pB_in_gg(x0, x1)
U5_g(x0, x1)
U2_gg(x0, x1)
U6_g(x0)
U3_gg(x0)
From the DPs we obtained the following set of size-change graphs: